package at.tasat.io;

import java.util.Arrays;
import java.util.Comparator;

import at.tasat.assignment.Assignment;
import at.tasat.cnf.Literal;

public final class OutputFormatter {

	public static String getResultString(boolean sat, Assignment[] assignments) {
		if (sat) {
			Arrays.sort(assignments, new AssignmentComparator());
			StringBuilder string = new StringBuilder("s SATISFIABLE");
			string.append('\n');
			string.append('v');
			for (Assignment assignment : assignments) {
				string.append(' ');
				string.append(Literal.toLiteral(assignment.getVariableId(), assignment.getPhase()));
			}
			return string.toString().trim();
		} else {
			return "s UNSATISFIABLE";
		}
	}

	public static String getCommentString(String comment) {
		return getString('c', comment);
	}

	public static String getErrorString(Throwable t) {
		return getErrorString(toString(t));
	}

	private static String toString(Throwable t) {
		StringBuilder builder = new StringBuilder();
		builder.append(t.getClass().getName() + ": " + t.getMessage());
		for (StackTraceElement frame : t.getStackTrace()) {
			builder.append('\n');
			builder.append(frame.toString());
		}
		Throwable cause = t.getCause();
		if (cause != null) {
			builder.append('\n');
			builder.append(toString(cause));
		}
		return builder.toString();
	}

	public static String getErrorString(String description) {
		return getString('e', description);
	}

	private static String getString(char header, String str) {
		StringBuilder builder = new StringBuilder();
		for (String line : str.split("\n")) {
			builder.append(header);
			builder.append(' ');
			builder.append(line);
			builder.append('\n');
		}
		return builder.toString().trim();
	}

	private final static class AssignmentComparator implements Comparator<Assignment> {

		@Override
		public int compare(Assignment a1, Assignment a2) {
			return Integer.compare(a1.getVariableId(), a2.getVariableId());
		}

	}

	private OutputFormatter() {
		// nothing to do
	}

}
